:- use_module(library(clpfd)).
:- use_module(library(clpr)).
:- use_module(inequalities).
:- use_module(library(terms)).

% ####################### Top Level Interface ##########################




yed_mode.

:- dynamic stream_html/1,  interesting/2.


colour(new_solution, '#7777FF').
size(new_solution, 200).

%@  @item interesting(+Predicate. +Dimension)
%@  The predicate interesting can be used to define predicates that must be highlighted in the graph. The second argument
%@  is the desired dimension of the node.
interesting(ex(_,_), 610, '#00EEEE').
interesting(gpr(_,_), 310, '#EEEEEE').




%@  @item transform(+InFile)
%@ It will transform the proof tree in the given "InFile" to 
%@ a meaningful one and write it to "InFile.graphml"

transform(InFile) :-
	clear,
	[InFile],
	attach_leaves,
	atom_concat(InFile, '.graphml', OutFile),
	tell(OutFile),
	(yed_mode ->
		atom_concat(InFile, '.html', OutHtmlFile),
		open(OutHtmlFile, 'write', SH),
		retractall(stream_html(_)),
		assert(stream_html(SH)),
		init_html
		;
		true
	),
	dump_tree,
	told,
	(yed_mode ->
		close_html,
		close(SH)
		;
		true
	),
	clear.

% ------------- Detailed Implementation -----------------

dump_tree :-
	write_header,
		define_attrs,
		open_graph,
			dump_nodes,
			dump_edges,
		close_graph,
	write_footer.

write_header :-
	writeln('<?xml version="1.0" encoding="UTF-8" standalone="no"?>'),
	writeln('<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://graphml.graphdrawing.org/xmlns http://www.yworks.com/xml/schema/graphml/1.1/ygraphml.xsd" xmlns:y="http://www.yworks.com/xml/graphml">').


define_attrs :-
	twriteln('<key attr.name="description" attr.type="string" for="node" id="stateinfo"/>'), %legacy, can be used for additional info
	twriteln('<key attr.name="query" attr.type="string" for="node" id="q"/>'),
	twriteln('<key attr.name="type" attr.type="string" for="node" id="t"/>'),
	twriteln('<key attr.name="topgoal" attr.type="string" for="node" id="tg"/>'),
	twriteln('<key attr.name="goals" attr.type="string" for="node" id="gs"/>'),
	twriteln('<key attr.name="abducibles" attr.type="string" for="node" id="as"/>'),
	twriteln('<key attr.name="denials" attr.type="string" for="node" id="ds"/>'),
	twriteln('<key attr.name="constraints" attr.type="string" for="node" id="cs"/>'),
	twriteln('<key attr.name="info" attr.type="string" for="node" id="i"/>'), %This is used for additional info (depth, or score), captured in the last argument of st/4
	(yed_mode -> 
        	twriteln('<key for="node" id="d0" yfiles.type="nodegraphics"/>'), 
        	twriteln('<key id="d1" for="edge" yfiles.type="edgegraphics"/>'),
        	twriteln('<key attr.name="url" attr.type="string" for="node" id="d2"/>') 
	; 
	true).


open_graph :-
	twriteln('<graph edgedefault="directed">').

dump_nodes :-
	forall(st(ID, Type, Query-(Goals,Abducibles,Constraints,Denials), Info), (
		ttwrite('<node id="'), write(ID), writeln('">'),
		(yed_mode ->
			yed_tags(st(ID, Type, Query-(Goals,Abducibles,Constraints,Denials), Info)),
			yed_html(st(ID, Type, Query-(Goals,Abducibles,Constraints,Denials), Info))
		;
		%Type
			tttwriteln('<data key="t"><![CDATA['),
				write_info(t, (Type)),
			tttwriteln(']]></data>'),
		%TopGoal
			tttwriteln('<data key="tg"><![CDATA['),
				write_info(tg, (Goals)),
			tttwriteln(']]></data>'),
		%All the goals
			tttwriteln('<data key="gs"><![CDATA['),
				write_info(gs, (Goals)),
			tttwriteln(']]></data>'),
		%Abducibles	
			tttwriteln('<data key="as"><![CDATA['),
				write_info(as, (Abducibles)),
			tttwriteln(']]></data>'),
		%Constraints
			tttwriteln('<data key="cs"><![CDATA['),
				write_info(cs, (Constraints)),
			tttwriteln(']]></data>'),
		%Denials
			tttwriteln('<data key="ds"><![CDATA['),
				write_info(ds, (Denials)),
			tttwriteln(']]></data>'),
		%Info
			tttwriteln('<data key="i"><![CDATA['),
				write_info(i, (Info)),
			tttwriteln(']]></data>')
		),	
		ttwriteln('</node>')
	)).

write_info(t, (T)) :-
		(T=i ->
				twriteln('Intermediate')
		;
		T=f ->
				twriteln('Fail')
		;
				twriteln('Success')
		).
			
			
write_info(tg, (G)) :-
		((length(G, L),  L>0) ->
				G = [H | _],		%Getting only the first goal in the list
				derive_topgoal(H, HD),
				twriteln(HD)
			;
				true
		).


write_info(gs, (G)) :-
		(G \= [] ->
				forall(member(X, G), (
					twriteln(X)
				))
			;
				true
			).
			
write_info(as, (A)) :-
		(A \= [] ->
				forall(member(X, A), (
					twriteln(X)
				))
			;
				true
			).

write_info(cs, (C)) :-
		(C \= [] ->
				forall(member(X, C), (
					twriteln(X)
				))
			;
				true
			).

write_info(ds, (D)) :-
		(D \= [] ->
				forall(member(X, D), (
					twriteln(X)
				))
			;
				true
			).
	
%Usually case specific. It should resort to an external handler if structured
write_info(i, (I)) :-
		(I \= [] ->
				forall(member(X, I), (		
					twriteln(X)
				))
			;
				true
			).

dump_edges :-
	forall(arc(From, To), (
			ttwrite('<edge '),writelist(['source="',From,'" target="',To,'"']),writeln('/>')
		)
	).

close_graph :-
	twriteln('</graph>').	

write_footer :-
	writeln('</graphml>').

writelist([]).
writelist([H|T]) :-
	write(H), writelist(T).

twrite(X) :- write('\t'), write(X).
ttwrite(X) :- write('\t\t'), write(X).
tttwrite(X) :- write('\t\t\t'), write(X).

%writeln(X) :- write(X), nl.
twriteln(X) :- write('\t'), write(X), nl.
ttwriteln(X) :- write('\t\t'), write(X), nl.
tttwriteln(X) :- write('\t\t\t'), write(X), nl.
twriteln(S,X) :- is_stream(S), write(S, '\t'), write(S,X), write(S,'\n').
ttwriteln(S,X) :- is_stream(S), write(S, '\t\t'), write(S,X), write(S,'\n').
tttwriteln(S,X) :- is_stream(S), write(S, '\t\t\t'), write(S,X), write(S,'\n').

derive_topgoal(fail(Vs, [H | _]), forall(Vs, fail(H, '...')), neg) :- !.
derive_topgoal(X, X, pos).

derive_topgoal(fail(Vs, [H | _]), forall(Vs, fail(H))) :- !.
derive_topgoal(X, X).




% ### YED specific. Prints the tree in a nice coloured format

yed_html(st(ID, Type, _Query-(Goals,Abducibles,Constraints,Denials), Info)) :-
	stream_html(S),
	is_stream(S),
	twriteln(S, '<tr>'),
	twriteln(S, '<td>'),
			write(S, '<a name='), write(S, ID), write(S, '>'), write(S, ID), write(S, '</a>'), write(S, ' ('), write(S, Type), write(S, ')'),
	twriteln(S, '</td>'),
	twriteln(S, '<td>'),
			forall(member(X, Goals),
				(
					X = fail(Vs, List) ->
					write(S, 'forall: '), write(S, Vs), write(S,'   <BR>'),
					forall(member(Y, List),
							(		write(S, '-----'),			write(S, Y), write(S,'  <BR>')))
					;
					write(S, X), write(S,'   <BR>')
				)
			), 
	twriteln(S, '</td>'),
	twriteln(S, '<td>'),
			forall(member(X, Abducibles),
				(
				write(S, X), 
				write(S,'      <BR>')
				)
			), 
	twriteln(S, '</td>'),
	twriteln(S, '<td>'),
			forall(member(X, Constraints),
				(
				write(S, X), 
				write(S,'     <BR>')
				)
			), 
	twriteln(S, '</td>'),
	twriteln(S, '<td>'),
			forall(member(X, Denials),
				(
				write(S, X), 
				write(S,'     <BR>')
				)
			), 
	twriteln(S, '</td>'),
	twriteln(S, '<td>'),
				write(S, Info), 
	twriteln(S, '</td>'),
	twriteln(S, '</tr>').
				
init_html  :-
	stream_html(S),
	is_stream(S),
	twriteln(S, '<html><body><table border="1">').


close_html  :-
	stream_html(S),
	is_stream(S),
	twriteln( S, '</table></body></html>').
	
          
      
yed_tags(st(ID, Type, _Query-(Goals,Abducibles,_Constraints,_Denials), Info)) :- 
        length(Goals, LGoals),
        (LGoals > 0 ->
                        Goals = [H | _],
                        derive_topgoal(H, HD, GoalType)
                ;
                HD=''
        ),
        (
           Info = scr(_Depth-(_, Score)), number(Score), !;  
           Info = scr(_Depth-(Score, _)), number(Score), !; 
           Info = scr(_Depth-Score), number(Score), !; 
           Score = 0.5
        ),
        Dimension = 100,
        %%%Link to HTML
%        twrite('<data key="d2"><![CDATA['), 
%                write('file://'),      
%                write( - name of the html file - ),     write('#'),write(ID),
%       ttwriteln(']]></data>'),        
        %%%
        twriteln('<data key="d0">'),
        twriteln('<y:ShapeNode>'),
        twriteln('<y:Shape type="ellipse"/>'),
        twriteln('<y:Geometry height="30.0" width="30.0" x="165.0" y="81.0"/>'),
        ( 
           ( arc(From, ID), 
             st(From, _, _-(_,AbduciblesParent,_,_),_), 
             length(AbduciblesParent, APL), 
             length(Abducibles, AL),          
             AL > APL 
           ) -> %If it abduces something
                                colour(new_solution, NSC), size(new_solution, NSS),
                                writelist(['\t<y:Fill color="', NSC, '" transparent="false"/>']),
                                writelist(['\t<y:Geometry height="', NSS, '" width="', NSS, '"/>']),
                                twriteln('<y:NodeLabel modelName="sides" modelPosition="e" >'), 
                                listtoacapo(Abducibles, AbduciblesAC),
                                ttwriteln(AbduciblesAC),                
                                twriteln('</y:NodeLabel>')
          ; %If it doesn't abduce something
                                  ((interesting(HD, Size, Colour)) -> %...but it's interesting
                                               ( %...make it big and coloured
                                                twriteln('<y:Fill color="'), write(Colour), write('" transparent="false"/>'),
                                                writelist(['\t<y:Geometry height="', Size, '" width="', Size, '"/>'])
                                               ) 
                                   ; %...otherwise find the appropriate colour and keep the default dimension
                                            twriteln('<y:Geometry height="'), twriteln(Dimension), twriteln('" width="'), twriteln(Dimension), twriteln('"/>')
                                  )
          ),
          (Type=i -> %If it is an intermediate node
                        (GoalType = pos -> %If it is positive 
                                twriteln('<y:BorderStyle color="#000000" type="line" width="30.0"/>'),
                                (interesting(HD, Size, Colour) -> true ;  twriteln('<y:Fill color="#FFFFFF" transparent="false"/>'))
                                %twriteln('<y:Geometry height="'), twriteln(Dimension), twriteln('" width="'), twriteln(Dimension), twriteln('"/>')
                        ;%it's negative so it's black
                        twriteln('<y:BorderStyle color="#000000" type="line" width="30.0"/>'),
                        (interesting(HD, Size, Colour) -> true ; twriteln('<y:Fill color="#000000" transparent="false"/>'))
                        %twriteln('<y:Geometry height="'), twriteln(Dimension), twriteln('" width="'), twriteln(Dimension), twriteln('"/>')
                        )
                ;%Not intermediate
                Type=f -> %It's failure
                        twriteln('<y:BorderStyle color="#FF0000" type="line" width="15.0"/>'),
                        twriteln('<y:Geometry height="100.0" width="100.0"/>'),
                        (interesting(HD, Size, Colour) -> true ;twriteln('<y:Fill color="#FF6666" transparent="false"/>'))
                ; %It's success
                        twriteln('<y:Shape type="rectangle"/>'),
                        twriteln('<y:BorderStyle color="#00FF00" type="line" width="30.0"/>'),
                        (interesting(HD, Size, Colour) -> true ; twriteln('<y:Fill color="#66FF66" transparent="false"/>')),
                        twriteln('<y:Geometry height="200.0" width="200.0"/>')
                ),
        cdata(HD, CDHD),
        TCol = '#777777',
        write('\n<y:NodeLabel modelName="internal" modelPosition="c" textColor="'), write(TCol), write('">'),
                ttwriteln(ID),write('(s:'), write(Info), write(')'),    
                twriteln('</y:NodeLabel>'),             
        twriteln('<y:NodeLabel modelName="sandwich" modelPosition="s" >'), 
                ttwriteln(CDHD),                
                twriteln('</y:NodeLabel>'),     
        twriteln('</y:ShapeNode>'),
        twriteln('</data>').
        

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%Utilities

make_dimension(Score, 100) :-
        X is 1/Score * 50,
        X > 100, !.
make_dimension(Score, 10) :-
        X is 1/Score * 50,
        X < 10, !.
make_dimension(Score, X) :-
         X is 1/Score *50.

listtoacapo([],  '').
listtoacapo([H|T],  O) :-
        listtoacapo(T, OT),
        term_to_atom(H,HA),
        atom_concat(OT, '\n', OTC),
        atom_concat(OTC, HA, O).


%& - &amp;
%< - &lt;
%> - &gt;
%" - &quot;
%' - &#39;
cdata(HD, CDHD) :-
	replacewith('&', '&amp;', HD, HD1),
	replacewith('<', '&lt;', HD1, HD2),
	replacewith('>', '&gt;', HD2, HD3),
	replacewith('"', '&quot;', HD3, HD4),
	replacewith('\'', '&#39;', HD4, CDHD).			
	
	
replacewith(Replace, With, In, Out) :-
	atom_codes(Replace,R),
	atom_codes(With,W),
	term_to_atom(In,IA),	
	atom_codes(IA,I),
	replaceal(R,W,I,O),
	atom_codes(Out,O).

%replaceal replaces one subset of a list with another... 
%replaceal("12","34","this12is12a12string",X0),atom_codes(XA,X0). 

replaceal(_,_,[],[]):-!. 
replaceal(X,Y,Lx,Lyj):- 
        matchR(X,Lx,LxN),!, 
        replaceal(X,Y,LxN,Lyi),!, 
        append(Y,Lyi,Lyj). 
replaceal(X,Y,[H|Lx],[H|Ly]):-!, 
        replaceal(X,Y,Lx,Ly). 
%Match and Replace... 
matchR([],X,X):-!. 
matchR([H|L1],[H|L2],X):-!, 
        matchR(L1,L2,X). 
        
        
        
%%%%%%%%%%%%%

% ### Basic Data Structure and Operations

:- dynamic st/4, arc/2.
:- dynamic sta_id_count/1.

clear :-
	retractall(st(_,_)),
	retractall(arc(_,_)).

attach_leaves :-
	findall(ID, st(ID, _), IDs),
	length(IDs, Len),
	retractall(sta_id_count(_)),
	assert(sta_id_count(Len)),
	attach_failure_leaves,
	attach_successful_leaves,
	retractall(sta_id_count(_)).

attach_failure_leaves :-
	findall(F, arc(F, []), Fs),
	forall(member(ID, Fs), (
		retract(arc(ID, [])),
		gen_sta_id(NewID),
		assertz(st(NewID, fail)),
		assertz(arc(ID, [NewID]))
	)).

attach_successful_leaves :-
	findall(F, arc(F, true), Fs),
	forall(member(ID, Fs), (
		retract(arc(ID, true)),
		gen_sta_id(NewID),
		assertz(st(NewID, succeed)),
		assertz(arc(ID, [NewID]))
	)).

gen_sta_id(ID) :-
	retract(sta_id_count(ID)),
	NewID is ID + 1,
	assert(sta_id_count(NewID)).


%Support for sicstus



% ------------------ For Quick Testing -------------------------
% :- transform('proof.out'). % FIXME: for testing only





% *** Utilities ***
:- if(current_prolog_flag(dialect, yap)).
%{

%}
:- elif(current_prolog_flag(dialect, sicstus)).
%{
forall(X, Y) :- \+ (X, \+ Y).

writeln(T) :-
        write(T),
        nl.  

is_stream(S) :-
        current_stream(_,_,S).

%}
:- endif.
